This book uses a variety of applications to illustrate a modeling method that helps practitioners to manage complex software-intensive systems. The proposed method relies on the combination of its abstraction concept and its operational character, with behavioral models in the precise and simple form of Abstract State Machines (ASMs). The book introduces both the modeling method (Part I) and the available tool support (Part II): In Part I the authors detail (using numerous examples) how to construct, explain, debug, explore, extend and reuse accurate system design models, starting from scratch. Only an elementary knowledge of common mathematical (including set-theoretic) notation and some basic experience with computational processes (systems, programs, algorithms) is assumed. Part II then shows how the modeling method can be supported by implementing tools that make design models executable and debuggable. To illustrate how to build, debug and maintain systems and to explain their construction in a checkable manner, a general, problem-oriented refinement method is adopted to construct system models from components. The method starts with abstract models and refines them step by step, incrementally adding further details that eventually lead to code. Intended for practitioners who build software intensive systems, and students specializing in software engineering, it can be used both for self-study and for teaching, and it can serve as a reference book. Exercises are included to help readers check their understanding of the explained concepts. For many models defined in the book, refinements to executable versions can be downloaded for experimental validation from the book's website at http://modelingbook.informatik.uni-ulm.de

Activities performed in organizations are coordinated via communication between the people involved. The sentences used to communicate are naturally structured by subject, verb, and object. The subject describes the actor, the verb the action and the object what is affected by the action. Subject-oriented Business Process Management (S-BPM) as presented in this book is based on this simple structure which enables process-oriented thinking and process modeling. S-BPM puts the subject of a process at the center of attention and thus deals with business processes and their organizational environment from a new perspective, meeting organizational requirements in a much better way than traditional approaches. Subjects represent agents of an action in a process, which can be either technical or human (e.g. a thread in an IT system or a clerk). A process structures the actions of each subject and coordinates the required communication among the subjects. S-BPM provides a coherent procedural framework to model and analyze business processes: its focus is the cooperation of all stakeholders involved in the strategic, tactical, and operational issues, sharing their knowledge in a networked structure. The authors illustrate how each modeling activity through the whole development lifecycle can be supported through the use of appropriate software tools. The presentation style focuses on professionals in industry, and on students specializing in process management or organizational modeling. Each chapter begins with a summary of key findings and is full of examples, hints, and possible pitfalls. An interpreter model, a toolbox, and a glossary summarizing the main terms complete the book. The web site www.i2pm.net provides additional software tools and further material.

The origin of this book goes back to the Dagstuhl seminar on Logic for System Engineering, organized during the first week of March 1997 by S. Jiihnichen, J. Loeckx, and M. Wirsing. During that seminar, after Egon Borger's talk on How to Use Abstract State Machines in Software Engineering, Wolfram Schulte, at the time a research assistant at the University of Ulm, Germany, questioned whether ASMs provide anything special as a scientifically well founded and rigorous yet simple and industrially viable framework for high level design and analysis of complex systems, and for natural refinements of models to executable code. Wolfram Schulte argued, referring to his work with K. Achatz on A Formal Object-Oriented Method Inspired by Fusion and Object-Z [1], that with current techniques of functional programming and of axiomatic specification, one can achieve the same result. An intensive and long debate arose from this discussion. At the end of the week, it led Egon Borger to propose a collaboration on a real-life specification project of Wolfram Schulte's choice, as a comparative field test of purely functional declarative methods and of their enhancement within an integrated abstract state-based operational (ASM) approach. After some hesitation, in May 1997 Wolfram Schulte accepted the offer and chose as the theme a high-level specification of Java and of the Java Virtual Machine.

Activities performed in organizations are coordinated via communication

between the people involved. The sentences used to communicate are naturally structured by subject, verb, and object. The subject describes the actor, the verb the action and the object what is affected by the action. Subject-oriented Business Process Management (S-BPM) as presented in this book is based on this simple structure which enables process-oriented thinking and process modeling.

S-BPM puts the subject of a process at the center of attention and thus

deals with business processes and their organizational environment from a new perspective, meeting organizational requirements in a much better way than traditional approaches. Subjects represent agents of an action in a process, which can be either technical or human (e.g. a thread in an IT system or a clerk). A process structures the actions of each subject and coordinates the required communication among the subjects. S-BPM provides a coherent procedural framework to model and analyze business processes: its focus is the cooperation of all stakeholders involved in the strategic, tactical, and operational issues, sharing their knowledge in a networked structure.

The authors illustrate how each modeling activity through the whole development lifecycle can be supported through the use of appropriate software tools. The presentation style focuses on professionals in industry, and on students specializing in process management or organizational modeling. Each chapter begins with a summary of key findings and is full of examples, hints, and possible pitfalls. An interpreter model, a toolbox, and a glossary summarizing the main terms complete the book. The web site www.i2pm.net provides additional software tools and further material."

Quelli che s'innamoran di pratica senza scienzia sono come 'l nocchieri ch'entra in navilio sanza timone o bussola, 1 che mai ha certezza dove si vada. - Leonardo da Vinci Ich habe oft bemerkt, dass wir uns durch allzuvieles Symbolisieren 2 die Sprache fu ..r die Wirklichkeit untu ..chtig machen. - Christian Morgenstern This is the place to express our thanks. First of all we thank all those who over the years have actively contributed to shaping the novel software design and analysis method explained in this book. They are too numerous to be mentioned here. They all appear in some way or the other on the following pages, in particular in the bibliographical and historical Chap. 9 which can be read independently of the book. We then thank those who have helped with detailed critical comments on the draft chapters to shape the way our arguments are presented in this book: M. B.. orger (Diron Mu ..nster), I. Craggs (IBMHursley),G. DelCastillo(SiemensMunc .. hen),U. Gl. asser(SimonFraser University, Vancouver,Canada),J. Huggins(Kettering University,Michigan, USA), B. Koblinger (IBM Heidelberg), P. Pa ..ppinghaus (Siemens Munc .. hen), A. Preller (Universit' e de Montpellier, France), M. -L. Potet (INP de Gre- ble, France),W. Reisig (Humboldt-Universit. at zu Berlin, Germany),H. Rust (Universit. at Cottbus, Germany), G. Schellhorn (Universit. at Augsburg, G- many), B. Thalheim (Universit. at Cottbus, Germany) and a dozen student generationsat Universita 'di Pisa. We thankM. Barmet(ETH Zur .. ich)for her solutions of the exercises in Chap. 8. We also thank L.

This state-of-the-art survey gives a systematic presentation of recent advances in the design and validation of computer architectures. The book covers a comprehensive range of architecture design and validation methods, from computer aided high-level design of VLSI circuits and systems to layout and testable design, including the modeling and synthesis of behavior and dataflow, cell-based logic optimization, machine assisted verification, and virtual machine design.

WorkonthisvolumestartedwiththeLipariSummerSchoolonAdvancesinSo- ware Engineering, which the ?rst editor organizedtogether with Alfredo Ferro fromtheUniversityofCataniainJuly2007.Itwasthe19thinawell-knownse- 1 riesofannualinternationalschools, addressedatcomputerscienceresearchers. Thethemesofthecourses, offourone-hourlectureseach, rangedfromdomain andrequirementsengineering(DinesBjoerner, TechnicalUniversityofDenmark, and Florin Spanachi, SAP Research, Germany) over high-level modeling (Egon B] orger, University of Pisa, Italy) and software product line techniques (Don Batory, UniversityofTexasatAustin, USA)toevolvablesoftware(PeterSestoft, Royal Veterinary and Agricultural University of Denmark) and the evolution of service-oriented software architectures (Carlo Ghezzi, Politecnico di Milano, Italy) in particular for Web services (Boualem Benatallah, University of New SouthWales, Australia)andthecrucialproblemofhowtoreachsecurity insuch evolvingdistributedsystems(DieterGollmann, TechnicalUniversityHamburg- Harburg, Germany). In two seminars the theme of evolvable software was further developed by the presentationofnew techniques forsoftwaremanipulation with annotations in Java (Vincenzo Gervasi, University of Pisa) and for the code-bricks-based runtime composition of self-evolving programs (Antonio Cisternino, University ofPisa). For unforseeablepersonalcircumstances MichaelJackson(London)was - abletodeliverhislecturesasplanned.However, thisvolumecontainshisre?- tions on which directions software engineering should take to become a truly engineeringdiscipline. This book is not a proceedings volume, but a collection of research papers on themes treated in the school, written with the intent to produce a state-- the art compendium of recent advances in software engineering. However, the contributions re?ect the extensive discussions we had during the two weeks in Lipari. Allcontributions, writtenbetweenAugust2007andJanuary2008, havebeen reviewed, revisedandreviewedagainduringtheperiodFebruary-August2008. We thank the 21 reviewers for their considerable and very constructive work, althoughasusualtheyhavetoremainanonymous.Lastbutnotleastwethank theauthorsfortheircommitmen

This book constitutes the refereed proceedings of the First International Conference of Abstract State Machines, B and Z, ABZ 2008, held in London, UK, in September 2008. The conference simultaneously incorporated the 15th International ASM Workshop, the 17th International Conference of Z Users and the 8th International Conference on the B Method.

The 44 revised full papers presented together with 4 invited contributions were carefully reviewed and selected from numerous submissions. The conference fosters the cross-fertilization of three rigorous methods for the design and analysis of hardware and software systems - both in academia and industry - namely Abstract State Machines, B, and Z. Covering a wide range of research spanning from theoretical and methodological foundations to tool support and practical applications, the contributions are organized in topical sections on abstract state machines, B papers, Z papers, ABZ short papers, and the papers of the Verified Software Repository Network (VSR-net) workshop.

The systems engineering method proposed in this book, which is based on Abstract State Machines (ASMs), guides the development of software and embedded hardware-software systems seamlessly from requirements capture to actual implementation and documentation. The method bridges the gap between the human understanding and formulation of real-world problems and the deployment of their algorithmic solutions by code-executing machines. Within a single conceptual framework it covers design, verification by reasoning techniques, and validation by simulation and testing. ASMs improve current industrial practice by using accurate high-level modeling and by linking the descriptions at the successive stages of system development in an organic and efficiently maintainable chain of rigorous and coherent system models at stepwise-refined abstraction levels. In several industrial projects the ASM method has proven its superiority compared to the popular UML methodology when designing complex parallel or dynamic systems. This book combines the features of a textbook and a handbook: the reader will find detailed explanations, proofs, and exercises as well as numerous examples and real-world case studies. Researchers will find here the most comprehensive description of ASMs available today and professionals will use it as a "modeling handbook for the working software engineer." As a textbook it supports self-study or it can form the basis of a lecture course. The book is complemented by a CD containing the whole book text, additional course material, solutions to exercises, and additional examples. Even more information can be found on the related website maintained by the authors: http://www.di.unipi.it/AsmBook/

This book constitutes the refereed proceedings of the 10th International Workshop on Abstract State Machines, ASM 2003, held in Taormina, Italy in March 2003. The 16 revised full papers presented together with 8 invited papers and 12 abstracts were carefully reviewed and selected for inclusion in the book. The papers reflect the state of the art of the abstract state machine method for the design and analysis of complex software/hardware systems. Besides theoretical results and methodological progress, application in various fields are studied as well.

This is the most comprehensive treatment available in book form of the classical decision problem of mathematical logic and of the role of the classical decision problem in modern computer science. A revealing analysis of the natural order of decidable and undecidable cases is given. The complete classification of the solvable and unsolvable standard cases of the classical decision problem will be of particular interest to the reader. The classification comes complete with the complexity analysis of the solvable cases, with the comprehensive treatment of the reduction method, and with the model-theoretical analysis of solvable cases. Many cases are treated here for the first time, and a great number of simple proofs and exercises have been included. The results and methods of the book are extensively used in logic, computer science and artificial intelligence.

This state-of-the-art survey gives a systematic presentation of recent advances in the design and validation of computer architectures. Based on advanced research ideas and approaches, and written by eminent researchers in the field, seven chapters cover the whole range from computer aided high-level design of VLSI circuits and systems to layout and testable design, including modeling and synthesis of behavior, of control, and of dataflow, cell based logic optimization, machine assisted verification, and virtual machine design. The chapters presuppose only basic familiarity with computer architecture. They are self-contained and lead the reader gently and informatively to the forefront of current research. A special feature of the book is the comprehensive range of architecture design and validation topics covered, giving the reader a clear view of the problems and of advanced techniques for their solution.

This book, with the CD-ROM included, is the documentation of a unique collaborative effort in evaluating formal methods for usage under industrial constraints: the major techniques for formally supported specification, design, and verification of large programs and complex systems are applied to a non-trivial and non-academic problem which is typical for industrial informal requirements specifications.
The 21 papers included in the book, together with an introduction and competition report, were selected from 33 candidate solutions. This book comes with a CD-ROM containing, besides the printed papers, executable code, full definitions of all parts of the specifications, and detailed descriptions of foundational matters where appropriate.

This volume contains the final versions of a collection of papers presented at the Annual Conference of the European Association for Computer Science Logic, CSL '93, held at Swansea, UK in September 1993.
The 21 full papers included were selected from a total of 62 submissions and essentially contribute to the whole area of computer science logic research. They are devoted to such topics as set constraints, lambda calculi, process algebras, program semantics, intuitionistic logics, fixed-point logics, the equivalence problem, Horn clauses, quantifiers, and proof tranformations.

This volume presents the proceedings of the Computer Science Logic Workshop CSL '92, held in Pisa, Italy, in September/October 1992. CSL '92 was the sixth of the series and the first one held as Annual Conference of the European Association for Computer Science Logic (EACSL). Full versions of the workshop contributions were collected after their presentation and reviewed. On the basis of 58 reviews, 26 papers were selected for publication, and appear here in revised final form. Topics covered in the volume include: Turing machines, linear logic, logic of proofs, optimization problems, lambda calculus, fixpoint logic, NP-completeness, resolution, transition system semantics, higher order partial functions, evolving algebras, functional logic programming, inductive definability, semantics of C, classes for a functional language, NP-optimization problems, theory of types and names, sconing and relators, 3-satisfiability, Kleene's slash, negation-complete logic programs, polynomial-time oracle machines, and monadic second-order properties.

The workshop Computer Science Logic '90 was held at the Max-Planck-Haus in Heidelberg, Germany, October 1-5, 1990. It was the fourth in a series of worskhops, following CSL '89 at the University of Kaiserslautern (see LNCS 440), CSL '88 at the University of Duisberg (see LNCS 385), and CSL '87 at the University of Karlsruhe (see LNCS 329). This volume contains 24 papers, chosen by means of a review procedure from the 35 papers presented at the workshop, some of which were invited and some selected from a total of 89 submissions. The papers cover a wide range of topics arising from the applications of logic to computer science.

This volume contains the revised versions of 28 papers presented at the third workshop on Computer Science Logic held in Kaiserslautern, FRG, October 2-6, 1989. These proceedings cover a wide range of topics both from theoretical and applied areas of computer science. More specifically, the papers deal with problems arising at the border of logic and computer science, e.g. in complexity, data base theory, logic programming, artificial intelligece, and temporal logic. The volume should be of interest to all logicians and computer scientists working in the above field.

This volume contains the papers which were presented to the workshop "Computer-Science Logic" held in Karlsruhe on October 12-16, 1987. Traditionally Logic, or more specifically, Mathematical Logic splits into several subareas: Set Theory, Proof Theory, Recursion Theory, and Model Theory. In addition there is what sometimes is called Philosophical Logic which deals with topics like nonclassical logics and which for historical reasons has been developed mainly at philosphical departments rather than at mathematics institutions. Today Computer Science challenges Logic in a new way. The theoretical analysis of problems in Computer Science for intrinsic reasons has pointed back to Logic. A broad class of questions became visible which is of a basically logical nature. These questions are often related to some of the traditional disciplines of Logic but normally without being covered adequately by any of them. The novel and unifying aspect of this new branch of Logic is the algorithmic point of view which is based on experiences people had with computers. The aim of the "Computer-Science Logic" workshop and of this volume is to represent the richness of research activities in this field in the German-speaking countries and to point to their underlying general logical principles.

This volume contains 37 invited research papers collected in memory of Dieter R dding, who is known for his work on the classification of recursive functions, on reduction classes, on the spectrum problem and on the complexity of cardinality quantifiers in predicate logic and in arithmetical hierarchy. He was one of the first to pursue the interaction of logic and computer science. The volume reflects the wide spectrum of Dieter R dding's scientific interests.

This book provides a high-level description, together with a mathematical and an experimental analysis, of Java and of the Java Virtual Machine (JVM), including a standard compiler of Java programs to JVM code and the security critical bytecode verifier component of the JVM. The description is structured into language layers and machine components. It comes with a natural executable refinement (written in AsmGofer and provided on CD ROM) which can be used for testing code. The method developed for this purpose is based on Abstract State Machines (ASMs) and can be applied to other virtual machines and to other programming languages as well. The book is written for advanced students and for professionals and practitioners in research and development who need a complete and transparent definition and an executable model of the language and of the virtual machine underlying its intended implementation.The CD ROM contains the entire text of the book and numerous examples and exercises.

Thema dieses Buches sind zwei schon Voh Leibniz als zusammengehoerend erkannte Begriffe, deren mathematische Entwicklung von Frege bis Turing das theoretische Fundament der Computerwissenschaft gelegt hat: der Be- griff formaler Sprache als Trager prazisen Ausdrucks von Bedeutungen, Sach- verhalten, Problemen und der des Algorithmus oder Kalkuls, d. h. formal ope- rierender Verfahren zur Loesung prazis beschriebener Fragen und Probleme. Das Buch gibt eine einheitliche Einfuhrung in die moderne Theorie dieser Begriffe, wie sie sich zuerst in der mathematischen Logik und der Berechen- barkeitstheorie und weiter in der Automatentheorie, der Theorie formaler Sprachen und der Komplexitatstheorie entwickelt hat. Neben der Berucksich- tigung eines schon klassisch gewordenen Grundkanons dieser Gebiete ist die Stoffauswahl mit der Absicht getroffen worden, durchgangig Erneuerungen traditioneller Fragestellungen, Ergebnisse und Methoden den Vorrang zu ge- ben, die sich aus Bedurfnissen oder Erkenntnissen der Informatik und hier besonders der Komplexitatstheorie heraus entwickelt haben. Die Zielsetzung dieses Buches ist eine doppelte: Lehrbuch zu sein. fur Anfangervorlesungen zu den genannten Gebieten, wie sie in fast allen Curri- cula der Informatik, der Logik und der Mathematik heute auftreten, aber daruberhinaus auch Monographie, indem in systematischer Absicht in jedem der angesprochenen Gebiete weiterfuhrende Ergebnisse neuerer Forschungen (grossenteils erstmalig in lehrbuchartiger Form) vorgefuhrt werden und uber- all versucht wird, Analogien und Zusammenhange zwischen verschiedenen Be- griffen und Konstruktionen explizit herauszuarbeiten.